ds:x:Id fp Type, k:Knd, x:Id, n:, f:Top.
update-spec-decl(update-spec1(k;x;n;s,v.f(s,v));ds)  x  dom(ds) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, , Top, x.A(x), P  Q, False, A, AB, , {x:A| B(x) }, x:AB(x), IdDeq, x  dom(f), b, s = t, Prop, P  Q, P & Q, P  Q, type List, nil, car.cdr, (x  l), x:AB(x), {T}, update-spec-vars(upd), update-spec-decl(upd;ds), update-spec1(k;x;n;s,v.f(s;v)), SQType(T), s ~ t, Atom$n
Lemmas	Id sq, iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, iff wf, l member wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, top wf, nat wf, Knd wf, fpf wf, Id wf